p:FinProbSpace, n:, Y:RandomVariable(p;n). 0  Y  0  E(n;Y) 

latex

Definitions	Type, , x:A. B(x), t  T, True, E(n;F), , x:AB(x), P  Q, T, , r  s, P  Q, x:A  B(x), P & Q, P  Q, X  Y, RandomVariable(p;n), , FinProbSpace, #$n, rv-const(a)
Lemmas	expectation-monotone, finite-prob-space wf, nat wf, random-variable wf, rv-le wf, rv-const wf, qle wf, squash wf, true wf, rationals wf, expectation-rv-const, int inc rationals, expectation wf